Step of Proof: nequal_wf
9,38
postcript
pdf
Inference at
*
I
of proof for Lemma
nequal
wf
:
A
:Type,
x
,
y
:
A
.
x
y
A
latex
by ((Unfold `nequal` 0)
CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n
C
)) (first_tok :t) inil_term)))
latex
C
.
Definitions
a
b
T
,
,
t
T
,
x
:
A
.
B
(
x
)
Lemmas
not
wf
origin